(declare-fun P_error (Int Int Int) Bool)
(declare-fun P1 (Int Int Int) Bool)
(declare-fun P0 (Int Int Int) Bool)
(declare-fun query (Int Int) Bool)
(assert (forall ((local!0 Int)) (P0 local!0 0 local!0)))
(assert (forall ((local!0 Int) (c_local!2 Int)) (or (not (P_error (+ 1 local!0) 0 c_local!2)) (P1 local!0 1 (+ 2 c_local!2)))))
(assert (forall ((c_local!18 Int) (local!0 Int) (call_2_ex_status Int)) (let ((a!1 (not (and (P_error (+ 1 local!0) call_2_ex_status c_local!18) (not (= call_2_ex_status 0)))))) (or a!1 (P1 local!0 call_2_ex_status c_local!18)))))
(assert (forall ((local!0 Int) (c_local!24 Int)) (or (not (P0 (+ 2 local!0) 0 c_local!24)) (P_error local!0 4 c_local!24))))
(assert (forall ((local!0 Int) (call_0_ex_status Int) (c_local!26 Int)) (let ((a!1 (not (and (P0 (+ 2 local!0) call_0_ex_status c_local!26) (not (= call_0_ex_status 0)))))) (or a!1 (P_error local!0 call_0_ex_status c_local!26)))))
(assert (forall ((out_local!28 Int) (local!0 Int) (static!1 Int)) (or (not (P1 local!0 1 out_local!28)) (query local!0 static!1))))
(assert (forall ((out_local!28 Int) (local!0 Int) (ex_status Int) (static!1 Int)) (not (and (P1 local!0 ex_status out_local!28) (query local!0 static!1) (not (= ex_status 1))))))
(check-sat)
